Proof of proveit.physics.quantum.QPE._psi_t_output theorem¶

import proveit
from proveit import defaults, ExprTuple, ExprRange
from proveit import k, m, s, t, U
from proveit.numbers import (
    Mult, Exp, zero, one, two, subtract, exp2pi_i)
from proveit.linear_algebra import MatrixExp, TensorProd
from proveit.physics.quantum import var_ket_u, varphi
from proveit.physics.quantum.circuits import (
    QcircuitEquiv, phase_kickbacks_on_register)
from proveit.physics.quantum.QPE import (
    _s, _t, _ket_u, _U, _phase, _s_in_nat_pos, _u_ket_register, 
    _normalized_ket_u, _unitary_U, _phase_in_interval, _eigen_uu,
    QPE1_def, _psi_t_def, _psi_t_ket_is_normalized_vec)
theory = proveit.Theory() # the theorem's theory

%proving _psi_t_output

_psi_t_output

defaults.assumptions = _psi_t_output.conditions

# don't combine factors of 2
Mult.change_simplification_directives(combine_all_exponents=False, 
                                      combine_numeric_rational_exponents=False)

_psi_t_def

_psi_t = _psi_t_def.instantiate()

_psi_t_ket_is_normalized_vec

_psi_t_ket_is_normalized_vec.instantiate()

target_circuit = _psi_t_output.instance_expr.lhs.operand

QPE1_def

QPE1_inst = QPE1_def.instantiate({s:_s, U:_U})

phase_kickbacks_on_register

Uexponentials = ExprTuple(ExprRange(k, MatrixExp(_U, Exp(two, k)), 
                                    subtract(t, one), zero, order='decreasing'))

phases = ExprTuple(ExprRange(k, Mult(Exp(two, k), _phase), 
                             subtract(t, one), zero, order='decreasing'))

kickbacks = phase_kickbacks_on_register.instantiate(
    {m:_s, U:Uexponentials, var_ket_u:_ket_u, varphi:phases})

kickbacks_with_QPE1 = QPE1_inst.sub_left_side_into(
    kickbacks.inner_expr().lhs.operand)

For psi_t_tensor_u_expansion to simplify properly, we need to specify this default vector-space field, but we should be able to automate this in the future:

from proveit.numbers import Complex
from proveit.linear_algebra import VecSpaces
VecSpaces.default_field = Complex

psi_t_tensor_u__expansion = _psi_t.substitution(TensorProd(_psi_t.lhs, _ket_u))

output_consolidation = kickbacks_with_QPE1.lhs.operand.output_consolidation(
    replacements=[psi_t_tensor_u__expansion.derive_reversed()])

output_consolidation_from_desired = _psi_t_output.instance_expr.lhs.operand.output_consolidation()

equiv = output_consolidation.apply_transitivity(output_consolidation_from_desired)

equiv.sub_right_side_into(kickbacks_with_QPE1)

_psi_t_output may now be readily provable (assuming required theorems are usable).  Simply execute "%qed".

%qed

proveit.physics.quantum.QPE._psi_t_output has been proven.

	step type	requirements	statement
0	generalization	1	⊢
1	instantiation	4, 2, 3	⊢
	: , : , :
2	instantiation	4, 5, 6	⊢
	: , : , :
3	instantiation	7, 8, 9	⊢
	: , : , :
4	conjecture		⊢
	proveit.physics.quantum.circuits.rhs_prob_via_equiv
5	instantiation	10, 463, 751, 11, 12, 303, 13, 14, 15, 744, 746, 272, 16^*	⊢
	: , : , : , : , :
6	modus ponens	17, 18	⊢
7	conjecture		⊢
	proveit.physics.quantum.circuits.equiv_transitivity
8	modus ponens	19, 20	⊢
9	instantiation	31, 21	⊢
	: , :
10	conjecture		⊢
	proveit.physics.quantum.circuits.phase_kickbacks_on_register
11	instantiation	601, 22, 651, 360	⊢
	: , : , : , :
12	modus ponens	23, 24	⊢
13	axiom		⊢
	proveit.physics.quantum.QPE._normalized_ket_u
14	instantiation	601, 25, 651, 360	⊢
	: , : , : , :
15	modus ponens	26, 27	⊢
16	instantiation	688, 674, 736, 689, 28, 29, 690, 712, 693, 702, 703, 692	, ⊢
	: , : , : , : , : , :
17	instantiation	47, 748, 469, 30	⊢
	: , : , : , : , : , : , : , :
18	instantiation	31, 32	⊢
	: , :
19	instantiation	47, 736, 748, 689, 48, 690	⊢
	: , : , : , : , : , : , : , :
20	instantiation	670, 33, 34	⊢
	: , : , :
21	modus ponens	35, 36	⊢
22	instantiation	670, 37, 416	⊢
	: , : , :